Left Termination of the query pattern
tree_member(a,g)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

tree_member(X, tree(X, X1, X2)).
tree_member(X, tree(X3, Left, X4)) :- tree_member(X, Left).
tree_member(X, tree(X5, X6, Right)) :- tree_member(X, Right).

Query: tree_member(a,g)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: tree_member(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: tree_member(T1, T2), SCOPE: 1, CLAUSE: 0 | tree_member(T1, T2), SCOPE: 1, CLAUSE: 1 | tree_member(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | tree_member(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 1 | tree_member(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: tree_member(T1, T2), SCOPE: 1, CLAUSE: 1 | tree_member(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, T2) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: tree_member(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 1 | tree_member(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: tree_member(T17, T15) | tree_member(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: tree_member(T17, T15), SCOPE: 2, CLAUSE: 0 | tree_member(T17, T15), SCOPE: 2, CLAUSE: 1 | tree_member(T17, T15), SCOPE: 2, CLAUSE: 2 | ?_2 | tree_member(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: tree_member(T17, T15), SCOPE: 2, CLAUSE: 0\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: tree_member(T17, T15), SCOPE: 2, CLAUSE: 1 | tree_member(T17, T15), SCOPE: 2, CLAUSE: 2 | ?_2 | tree_member(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: tree_member(T17, T15), SCOPE: 2, CLAUSE: 1\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: tree_member(T17, T15), SCOPE: 2, CLAUSE: 2 | ?_2 | tree_member(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: tree_member(T53, T51)\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: tree_member(T17, T15), SCOPE: 2, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ?_2 | tree_member(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: tree_member(T80, T79)\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: tree_member(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: tree_member(T106, T105)\n\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: tree_member(T121, T119) | tree_member(T1, tree(T118, T119, T120)), SCOPE: 1, CLAUSE: 2\n\nT118 is ground\nT119 is ground\nT120 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, T119, T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: tree_member(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, T2) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: tree_member(T121, T119), SCOPE: 3, CLAUSE: 0 | tree_member(T121, T119), SCOPE: 3, CLAUSE: 1 | tree_member(T121, T119), SCOPE: 3, CLAUSE: 2 | ?_3 | tree_member(T1, tree(T118, T119, T120)), SCOPE: 1, CLAUSE: 2\n\nT118 is ground\nT119 is ground\nT120 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, T119, T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: tree_member(T121, T119), SCOPE: 3, CLAUSE: 0\n\nT118 is ground\nT119 is ground\nT120 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, T119, T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: tree_member(T121, T119), SCOPE: 3, CLAUSE: 1 | tree_member(T121, T119), SCOPE: 3, CLAUSE: 2 | ?_3 | tree_member(T1, tree(T118, T119, T120)), SCOPE: 1, CLAUSE: 2\n\nT118 is ground\nT119 is ground\nT120 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, T119, T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: tree_member(T121, T119), SCOPE: 3, CLAUSE: 1\n\nT118 is ground\nT119 is ground\nT120 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, T119, T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: tree_member(T121, T119), SCOPE: 3, CLAUSE: 2 | ?_3 | tree_member(T1, tree(T118, T119, T120)), SCOPE: 1, CLAUSE: 2\n\nT118 is ground\nT119 is ground\nT120 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, T119, T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: tree_member(T157, T155)\n\nT118 is ground\nT120 is ground\nT154 is ground\nT155 is ground\nT156 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, tree(T154, T155, T156), T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: tree_member(T121, T119), SCOPE: 3, CLAUSE: 2\n\nT118 is ground\nT119 is ground\nT120 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, T119, T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ?_3 | tree_member(T1, tree(T118, T119, T120)), SCOPE: 1, CLAUSE: 2\n\nT118 is ground\nT119 is ground\nT120 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, T119, T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: tree_member(T184, T183)\n\nT118 is ground\nT120 is ground\nT181 is ground\nT182 is ground\nT183 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, tree(T181, T182, T183), T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: tree_member(T1, tree(T118, T119, T120)), SCOPE: 1, CLAUSE: 2\n\nT118 is ground\nT119 is ground\nT120 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T118, T119, T120)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: tree_member(T210, T209)\n\nT207 is ground\nT208 is ground\nT209 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T207, T208, T209)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: tree_member(T225, T224)\n\nT222 is ground\nT223 is ground\nT224 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T222, T223, T224)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: tree_member(T225, T224), SCOPE: 4, CLAUSE: 0 | tree_member(T225, T224), SCOPE: 4, CLAUSE: 1 | tree_member(T225, T224), SCOPE: 4, CLAUSE: 2\n\nT222 is ground\nT223 is ground\nT224 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T222, T223, T224)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: tree_member(T225, T224), SCOPE: 4, CLAUSE: 0\n\nT222 is ground\nT223 is ground\nT224 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T222, T223, T224)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: tree_member(T225, T224), SCOPE: 4, CLAUSE: 1 | tree_member(T225, T224), SCOPE: 4, CLAUSE: 2\n\nT222 is ground\nT223 is ground\nT224 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T222, T223, T224)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: tree_member(T225, T224), SCOPE: 4, CLAUSE: 1\n\nT222 is ground\nT223 is ground\nT224 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T222, T223, T224)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: tree_member(T225, T224), SCOPE: 4, CLAUSE: 2\n\nT222 is ground\nT223 is ground\nT224 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T222, T223, T224)) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: tree_member(T261, T259)\n\nT222 is ground\nT223 is ground\nT258 is ground\nT259 is ground\nT260 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T222, T223, tree(T258, T259, T260))) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: tree_member(T280, T279)\n\nT222 is ground\nT223 is ground\nT277 is ground\nT278 is ground\nT279 is ground\nX10 is free\nX11 is free\nX12 is free\ntree_member(T1, tree(T222, T223, tree(T277, T278, T279))) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 55 [arrowhead = none ];
55 -> 2;

56 [label="EVAL with clause\ntree_member(X10, tree(X10, X11, X12)).\nand substitutionT1 -> T6,\nX10 -> T6,\nX11 -> T7,\nX12 -> T8,\nT2 -> tree(T6, T7, T8)", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 56 [arrowhead = none ];
56 -> 3;

57 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 57 [arrowhead = none ];
57 -> 4;

58 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 58 [arrowhead = none ];
58 -> 5;

59 [label="EVAL with clause\ntree_member(X116, tree(X117, X118, X119)) :- tree_member(X116, X118).\nand substitutionT1 -> T121,\nX116 -> T121,\nX117 -> T118,\nX118 -> T119,\nX119 -> T120,\nT2 -> tree(T118, T119, T120),\nT117 -> T121", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 59 [arrowhead = none ];
59 -> 23;

60 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 60 [arrowhead = none ];
60 -> 24;

61 [label="ONLY EVAL with clause\ntree_member(X17, tree(X18, X19, X20)) :- tree_member(X17, X19).\nand substitutionT1 -> T17,\nX17 -> T17,\nT6 -> T14,\nX18 -> T14,\nT7 -> T15,\nX19 -> T15,\nT8 -> T16,\nX20 -> T16,\nT13 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 61 [arrowhead = none ];
61 -> 6;

62 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
6 -> 62 [arrowhead = none ];
62 -> 7;

63 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
7 -> 63 [arrowhead = none ];
63 -> 8;

64 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
7 -> 64 [arrowhead = none ];
64 -> 9;

65 [label="EVAL with clause\ntree_member(X33, tree(X33, X34, X35)).\nand substitutionT17 -> T30,\nX33 -> T30,\nX34 -> T31,\nX35 -> T32,\nT15 -> tree(T30, T31, T32)", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 65 [arrowhead = none ];
65 -> 10;

66 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 66 [arrowhead = none ];
66 -> 11;

67 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 67 [arrowhead = none ];
67 -> 13;

68 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 68 [arrowhead = none ];
68 -> 14;

69 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 69 [arrowhead = none ];
69 -> 12;

70 [label="EVAL with clause\ntree_member(X52, tree(X53, X54, X55)) :- tree_member(X52, X54).\nand substitutionT17 -> T53,\nX52 -> T53,\nX53 -> T50,\nX54 -> T51,\nX55 -> T52,\nT15 -> tree(T50, T51, T52),\nT49 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 70 [arrowhead = none ];
70 -> 15;

71 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 71 [arrowhead = none ];
71 -> 16;

72 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 72 [arrowhead = none ];
72 -> 17;

73 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 73 [arrowhead = none ];
73 -> 18;

74 [label="INSTANCE with matching:\nT1 -> T53\nT2 -> T51", fontsize=14, style = filled, fillcolor = lightgrey];
15 -> 74 [arrowhead = none , style=dashed];
74 -> 1[style=dashed];

75 [label="EVAL with clause\ntree_member(X78, tree(X79, X80, X81)) :- tree_member(X78, X81).\nand substitutionT17 -> T80,\nX78 -> T80,\nX79 -> T77,\nX80 -> T78,\nX81 -> T79,\nT15 -> tree(T77, T78, T79),\nT76 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 75 [arrowhead = none ];
75 -> 19;

76 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 76 [arrowhead = none ];
76 -> 20;

77 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 77 [arrowhead = none ];
77 -> 21;

78 [label="INSTANCE with matching:\nT1 -> T80\nT2 -> T79", fontsize=14, style = filled, fillcolor = lightgrey];
19 -> 78 [arrowhead = none , style=dashed];
78 -> 1[style=dashed];

79 [label="ONLY EVAL with clause\ntree_member(X102, tree(X103, X104, X105)) :- tree_member(X102, X105).\nand substitutionT1 -> T106,\nX102 -> T106,\nT14 -> T103,\nX103 -> T103,\nT15 -> T104,\nX104 -> T104,\nT16 -> T105,\nX105 -> T105,\nT102 -> T106", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 79 [arrowhead = none ];
79 -> 22;

80 [label="INSTANCE with matching:\nT1 -> T106\nT2 -> T105", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 80 [arrowhead = none , style=dashed];
80 -> 1[style=dashed];

81 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
23 -> 81 [arrowhead = none ];
81 -> 25;

82 [label="EVAL with clause\ntree_member(X215, tree(X216, X217, X218)) :- tree_member(X215, X218).\nand substitutionT1 -> T225,\nX215 -> T225,\nX216 -> T222,\nX217 -> T223,\nX218 -> T224,\nT2 -> tree(T222, T223, T224),\nT221 -> T225", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 82 [arrowhead = none ];
82 -> 41;

83 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 83 [arrowhead = none ];
83 -> 42;

84 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
25 -> 84 [arrowhead = none ];
84 -> 26;

85 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
25 -> 85 [arrowhead = none ];
85 -> 27;

86 [label="EVAL with clause\ntree_member(X132, tree(X132, X133, X134)).\nand substitutionT121 -> T134,\nX132 -> T134,\nX133 -> T135,\nX134 -> T136,\nT119 -> tree(T134, T135, T136)", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 86 [arrowhead = none ];
86 -> 28;

87 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 87 [arrowhead = none ];
87 -> 29;

88 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
27 -> 88 [arrowhead = none ];
88 -> 31;

89 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
27 -> 89 [arrowhead = none ];
89 -> 32;

90 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 90 [arrowhead = none ];
90 -> 30;

91 [label="EVAL with clause\ntree_member(X151, tree(X152, X153, X154)) :- tree_member(X151, X153).\nand substitutionT121 -> T157,\nX151 -> T157,\nX152 -> T154,\nX153 -> T155,\nX154 -> T156,\nT119 -> tree(T154, T155, T156),\nT153 -> T157", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 91 [arrowhead = none ];
91 -> 33;

92 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 92 [arrowhead = none ];
92 -> 34;

93 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
32 -> 93 [arrowhead = none ];
93 -> 35;

94 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
32 -> 94 [arrowhead = none ];
94 -> 36;

95 [label="INSTANCE with matching:\nT1 -> T157\nT2 -> T155", fontsize=14, style = filled, fillcolor = lightgrey];
33 -> 95 [arrowhead = none , style=dashed];
95 -> 1[style=dashed];

96 [label="EVAL with clause\ntree_member(X177, tree(X178, X179, X180)) :- tree_member(X177, X180).\nand substitutionT121 -> T184,\nX177 -> T184,\nX178 -> T181,\nX179 -> T182,\nX180 -> T183,\nT119 -> tree(T181, T182, T183),\nT180 -> T184", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 96 [arrowhead = none ];
96 -> 37;

97 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 97 [arrowhead = none ];
97 -> 38;

98 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 98 [arrowhead = none ];
98 -> 39;

99 [label="INSTANCE with matching:\nT1 -> T184\nT2 -> T183", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 99 [arrowhead = none , style=dashed];
99 -> 1[style=dashed];

100 [label="ONLY EVAL with clause\ntree_member(X201, tree(X202, X203, X204)) :- tree_member(X201, X204).\nand substitutionT1 -> T210,\nX201 -> T210,\nT118 -> T207,\nX202 -> T207,\nT119 -> T208,\nX203 -> T208,\nT120 -> T209,\nX204 -> T209,\nT206 -> T210", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 100 [arrowhead = none ];
100 -> 40;

101 [label="INSTANCE with matching:\nT1 -> T210\nT2 -> T209", fontsize=14, style = filled, fillcolor = lightgrey];
40 -> 101 [arrowhead = none , style=dashed];
101 -> 1[style=dashed];

102 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
41 -> 102 [arrowhead = none ];
102 -> 43;

103 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
43 -> 103 [arrowhead = none ];
103 -> 44;

104 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
43 -> 104 [arrowhead = none ];
104 -> 45;

105 [label="EVAL with clause\ntree_member(X231, tree(X231, X232, X233)).\nand substitutionT225 -> T238,\nX231 -> T238,\nX232 -> T239,\nX233 -> T240,\nT224 -> tree(T238, T239, T240)", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 105 [arrowhead = none ];
105 -> 46;

106 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 106 [arrowhead = none ];
106 -> 47;

107 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 107 [arrowhead = none ];
107 -> 49;

108 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 108 [arrowhead = none ];
108 -> 50;

109 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 109 [arrowhead = none ];
109 -> 48;

110 [label="EVAL with clause\ntree_member(X250, tree(X251, X252, X253)) :- tree_member(X250, X252).\nand substitutionT225 -> T261,\nX250 -> T261,\nX251 -> T258,\nX252 -> T259,\nX253 -> T260,\nT224 -> tree(T258, T259, T260),\nT257 -> T261", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 110 [arrowhead = none ];
110 -> 51;

111 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 111 [arrowhead = none ];
111 -> 52;

112 [label="EVAL with clause\ntree_member(X268, tree(X269, X270, X271)) :- tree_member(X268, X271).\nand substitutionT225 -> T280,\nX268 -> T280,\nX269 -> T277,\nX270 -> T278,\nX271 -> T279,\nT224 -> tree(T277, T278, T279),\nT276 -> T280", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 112 [arrowhead = none ];
112 -> 53;

113 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 113 [arrowhead = none ];
113 -> 54;

114 [label="INSTANCE with matching:\nT1 -> T261\nT2 -> T259", fontsize=14, style = filled, fillcolor = lightgrey];
51 -> 114 [arrowhead = none , style=dashed];
114 -> 1[style=dashed];

115 [label="INSTANCE with matching:\nT1 -> T280\nT2 -> T279", fontsize=14, style = filled, fillcolor = lightgrey];
53 -> 115 [arrowhead = none , style=dashed];
115 -> 1[style=dashed];

}

(2) Obligation:

Clauses:

tree_memberA(T6, tree(T6, T7, T8)).
tree_memberA(T30, tree(T14, tree(T30, T31, T32), T16)).
tree_memberA(T53, tree(T14, tree(T50, T51, T52), T16)) :- tree_memberA(T53, T51).
tree_memberA(T80, tree(T14, tree(T77, T78, T79), T16)) :- tree_memberA(T80, T79).
tree_memberA(T106, tree(T103, T104, T105)) :- tree_memberA(T106, T105).
tree_memberA(T134, tree(T118, tree(T134, T135, T136), T120)).
tree_memberA(T157, tree(T118, tree(T154, T155, T156), T120)) :- tree_memberA(T157, T155).
tree_memberA(T184, tree(T118, tree(T181, T182, T183), T120)) :- tree_memberA(T184, T183).
tree_memberA(T210, tree(T207, T208, T209)) :- tree_memberA(T210, T209).
tree_memberA(T238, tree(T222, T223, tree(T238, T239, T240))).
tree_memberA(T261, tree(T222, T223, tree(T258, T259, T260))) :- tree_memberA(T261, T259).
tree_memberA(T280, tree(T222, T223, tree(T277, T278, T279))) :- tree_memberA(T280, T279).

Query: tree_memberA(a,g)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
tree_memberA_in: (f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

tree_memberA_in_ag(T6, tree(T6, T7, T8)) → tree_memberA_out_ag(T6, tree(T6, T7, T8))
tree_memberA_in_ag(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_memberA_out_ag(T30, tree(T14, tree(T30, T31, T32), T16))
tree_memberA_in_ag(T53, tree(T14, tree(T50, T51, T52), T16)) → U1_ag(T53, T14, T50, T51, T52, T16, tree_memberA_in_ag(T53, T51))
tree_memberA_in_ag(T80, tree(T14, tree(T77, T78, T79), T16)) → U2_ag(T80, T14, T77, T78, T79, T16, tree_memberA_in_ag(T80, T79))
tree_memberA_in_ag(T106, tree(T103, T104, T105)) → U3_ag(T106, T103, T104, T105, tree_memberA_in_ag(T106, T105))
tree_memberA_in_ag(T157, tree(T118, tree(T154, T155, T156), T120)) → U4_ag(T157, T118, T154, T155, T156, T120, tree_memberA_in_ag(T157, T155))
tree_memberA_in_ag(T184, tree(T118, tree(T181, T182, T183), T120)) → U5_ag(T184, T118, T181, T182, T183, T120, tree_memberA_in_ag(T184, T183))
tree_memberA_in_ag(T210, tree(T207, T208, T209)) → U6_ag(T210, T207, T208, T209, tree_memberA_in_ag(T210, T209))
tree_memberA_in_ag(T238, tree(T222, T223, tree(T238, T239, T240))) → tree_memberA_out_ag(T238, tree(T222, T223, tree(T238, T239, T240)))
tree_memberA_in_ag(T261, tree(T222, T223, tree(T258, T259, T260))) → U7_ag(T261, T222, T223, T258, T259, T260, tree_memberA_in_ag(T261, T259))
tree_memberA_in_ag(T280, tree(T222, T223, tree(T277, T278, T279))) → U8_ag(T280, T222, T223, T277, T278, T279, tree_memberA_in_ag(T280, T279))
U8_ag(T280, T222, T223, T277, T278, T279, tree_memberA_out_ag(T280, T279)) → tree_memberA_out_ag(T280, tree(T222, T223, tree(T277, T278, T279)))
U7_ag(T261, T222, T223, T258, T259, T260, tree_memberA_out_ag(T261, T259)) → tree_memberA_out_ag(T261, tree(T222, T223, tree(T258, T259, T260)))
U6_ag(T210, T207, T208, T209, tree_memberA_out_ag(T210, T209)) → tree_memberA_out_ag(T210, tree(T207, T208, T209))
U5_ag(T184, T118, T181, T182, T183, T120, tree_memberA_out_ag(T184, T183)) → tree_memberA_out_ag(T184, tree(T118, tree(T181, T182, T183), T120))
U4_ag(T157, T118, T154, T155, T156, T120, tree_memberA_out_ag(T157, T155)) → tree_memberA_out_ag(T157, tree(T118, tree(T154, T155, T156), T120))
U3_ag(T106, T103, T104, T105, tree_memberA_out_ag(T106, T105)) → tree_memberA_out_ag(T106, tree(T103, T104, T105))
U2_ag(T80, T14, T77, T78, T79, T16, tree_memberA_out_ag(T80, T79)) → tree_memberA_out_ag(T80, tree(T14, tree(T77, T78, T79), T16))
U1_ag(T53, T14, T50, T51, T52, T16, tree_memberA_out_ag(T53, T51)) → tree_memberA_out_ag(T53, tree(T14, tree(T50, T51, T52), T16))

The argument filtering Pi contains the following mapping:
tree_memberA_in_ag(x1, x2)  =  tree_memberA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
tree_memberA_out_ag(x1, x2)  =  tree_memberA_out_ag(x1)
U1_ag(x1, x2, x3, x4, x5, x6, x7)  =  U1_ag(x7)
U2_ag(x1, x2, x3, x4, x5, x6, x7)  =  U2_ag(x7)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x5)
U4_ag(x1, x2, x3, x4, x5, x6, x7)  =  U4_ag(x7)
U5_ag(x1, x2, x3, x4, x5, x6, x7)  =  U5_ag(x7)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x5)
U7_ag(x1, x2, x3, x4, x5, x6, x7)  =  U7_ag(x7)
U8_ag(x1, x2, x3, x4, x5, x6, x7)  =  U8_ag(x7)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

tree_memberA_in_ag(T6, tree(T6, T7, T8)) → tree_memberA_out_ag(T6, tree(T6, T7, T8))
tree_memberA_in_ag(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_memberA_out_ag(T30, tree(T14, tree(T30, T31, T32), T16))
tree_memberA_in_ag(T53, tree(T14, tree(T50, T51, T52), T16)) → U1_ag(T53, T14, T50, T51, T52, T16, tree_memberA_in_ag(T53, T51))
tree_memberA_in_ag(T80, tree(T14, tree(T77, T78, T79), T16)) → U2_ag(T80, T14, T77, T78, T79, T16, tree_memberA_in_ag(T80, T79))
tree_memberA_in_ag(T106, tree(T103, T104, T105)) → U3_ag(T106, T103, T104, T105, tree_memberA_in_ag(T106, T105))
tree_memberA_in_ag(T157, tree(T118, tree(T154, T155, T156), T120)) → U4_ag(T157, T118, T154, T155, T156, T120, tree_memberA_in_ag(T157, T155))
tree_memberA_in_ag(T184, tree(T118, tree(T181, T182, T183), T120)) → U5_ag(T184, T118, T181, T182, T183, T120, tree_memberA_in_ag(T184, T183))
tree_memberA_in_ag(T210, tree(T207, T208, T209)) → U6_ag(T210, T207, T208, T209, tree_memberA_in_ag(T210, T209))
tree_memberA_in_ag(T238, tree(T222, T223, tree(T238, T239, T240))) → tree_memberA_out_ag(T238, tree(T222, T223, tree(T238, T239, T240)))
tree_memberA_in_ag(T261, tree(T222, T223, tree(T258, T259, T260))) → U7_ag(T261, T222, T223, T258, T259, T260, tree_memberA_in_ag(T261, T259))
tree_memberA_in_ag(T280, tree(T222, T223, tree(T277, T278, T279))) → U8_ag(T280, T222, T223, T277, T278, T279, tree_memberA_in_ag(T280, T279))
U8_ag(T280, T222, T223, T277, T278, T279, tree_memberA_out_ag(T280, T279)) → tree_memberA_out_ag(T280, tree(T222, T223, tree(T277, T278, T279)))
U7_ag(T261, T222, T223, T258, T259, T260, tree_memberA_out_ag(T261, T259)) → tree_memberA_out_ag(T261, tree(T222, T223, tree(T258, T259, T260)))
U6_ag(T210, T207, T208, T209, tree_memberA_out_ag(T210, T209)) → tree_memberA_out_ag(T210, tree(T207, T208, T209))
U5_ag(T184, T118, T181, T182, T183, T120, tree_memberA_out_ag(T184, T183)) → tree_memberA_out_ag(T184, tree(T118, tree(T181, T182, T183), T120))
U4_ag(T157, T118, T154, T155, T156, T120, tree_memberA_out_ag(T157, T155)) → tree_memberA_out_ag(T157, tree(T118, tree(T154, T155, T156), T120))
U3_ag(T106, T103, T104, T105, tree_memberA_out_ag(T106, T105)) → tree_memberA_out_ag(T106, tree(T103, T104, T105))
U2_ag(T80, T14, T77, T78, T79, T16, tree_memberA_out_ag(T80, T79)) → tree_memberA_out_ag(T80, tree(T14, tree(T77, T78, T79), T16))
U1_ag(T53, T14, T50, T51, T52, T16, tree_memberA_out_ag(T53, T51)) → tree_memberA_out_ag(T53, tree(T14, tree(T50, T51, T52), T16))

The argument filtering Pi contains the following mapping:
tree_memberA_in_ag(x1, x2)  =  tree_memberA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
tree_memberA_out_ag(x1, x2)  =  tree_memberA_out_ag(x1)
U1_ag(x1, x2, x3, x4, x5, x6, x7)  =  U1_ag(x7)
U2_ag(x1, x2, x3, x4, x5, x6, x7)  =  U2_ag(x7)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x5)
U4_ag(x1, x2, x3, x4, x5, x6, x7)  =  U4_ag(x7)
U5_ag(x1, x2, x3, x4, x5, x6, x7)  =  U5_ag(x7)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x5)
U7_ag(x1, x2, x3, x4, x5, x6, x7)  =  U7_ag(x7)
U8_ag(x1, x2, x3, x4, x5, x6, x7)  =  U8_ag(x7)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

TREE_MEMBERA_IN_AG(T53, tree(T14, tree(T50, T51, T52), T16)) → U1_AG(T53, T14, T50, T51, T52, T16, tree_memberA_in_ag(T53, T51))
TREE_MEMBERA_IN_AG(T53, tree(T14, tree(T50, T51, T52), T16)) → TREE_MEMBERA_IN_AG(T53, T51)
TREE_MEMBERA_IN_AG(T80, tree(T14, tree(T77, T78, T79), T16)) → U2_AG(T80, T14, T77, T78, T79, T16, tree_memberA_in_ag(T80, T79))
TREE_MEMBERA_IN_AG(T80, tree(T14, tree(T77, T78, T79), T16)) → TREE_MEMBERA_IN_AG(T80, T79)
TREE_MEMBERA_IN_AG(T106, tree(T103, T104, T105)) → U3_AG(T106, T103, T104, T105, tree_memberA_in_ag(T106, T105))
TREE_MEMBERA_IN_AG(T106, tree(T103, T104, T105)) → TREE_MEMBERA_IN_AG(T106, T105)
TREE_MEMBERA_IN_AG(T157, tree(T118, tree(T154, T155, T156), T120)) → U4_AG(T157, T118, T154, T155, T156, T120, tree_memberA_in_ag(T157, T155))
TREE_MEMBERA_IN_AG(T184, tree(T118, tree(T181, T182, T183), T120)) → U5_AG(T184, T118, T181, T182, T183, T120, tree_memberA_in_ag(T184, T183))
TREE_MEMBERA_IN_AG(T210, tree(T207, T208, T209)) → U6_AG(T210, T207, T208, T209, tree_memberA_in_ag(T210, T209))
TREE_MEMBERA_IN_AG(T261, tree(T222, T223, tree(T258, T259, T260))) → U7_AG(T261, T222, T223, T258, T259, T260, tree_memberA_in_ag(T261, T259))
TREE_MEMBERA_IN_AG(T261, tree(T222, T223, tree(T258, T259, T260))) → TREE_MEMBERA_IN_AG(T261, T259)
TREE_MEMBERA_IN_AG(T280, tree(T222, T223, tree(T277, T278, T279))) → U8_AG(T280, T222, T223, T277, T278, T279, tree_memberA_in_ag(T280, T279))
TREE_MEMBERA_IN_AG(T280, tree(T222, T223, tree(T277, T278, T279))) → TREE_MEMBERA_IN_AG(T280, T279)

The TRS R consists of the following rules:

tree_memberA_in_ag(T6, tree(T6, T7, T8)) → tree_memberA_out_ag(T6, tree(T6, T7, T8))
tree_memberA_in_ag(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_memberA_out_ag(T30, tree(T14, tree(T30, T31, T32), T16))
tree_memberA_in_ag(T53, tree(T14, tree(T50, T51, T52), T16)) → U1_ag(T53, T14, T50, T51, T52, T16, tree_memberA_in_ag(T53, T51))
tree_memberA_in_ag(T80, tree(T14, tree(T77, T78, T79), T16)) → U2_ag(T80, T14, T77, T78, T79, T16, tree_memberA_in_ag(T80, T79))
tree_memberA_in_ag(T106, tree(T103, T104, T105)) → U3_ag(T106, T103, T104, T105, tree_memberA_in_ag(T106, T105))
tree_memberA_in_ag(T157, tree(T118, tree(T154, T155, T156), T120)) → U4_ag(T157, T118, T154, T155, T156, T120, tree_memberA_in_ag(T157, T155))
tree_memberA_in_ag(T184, tree(T118, tree(T181, T182, T183), T120)) → U5_ag(T184, T118, T181, T182, T183, T120, tree_memberA_in_ag(T184, T183))
tree_memberA_in_ag(T210, tree(T207, T208, T209)) → U6_ag(T210, T207, T208, T209, tree_memberA_in_ag(T210, T209))
tree_memberA_in_ag(T238, tree(T222, T223, tree(T238, T239, T240))) → tree_memberA_out_ag(T238, tree(T222, T223, tree(T238, T239, T240)))
tree_memberA_in_ag(T261, tree(T222, T223, tree(T258, T259, T260))) → U7_ag(T261, T222, T223, T258, T259, T260, tree_memberA_in_ag(T261, T259))
tree_memberA_in_ag(T280, tree(T222, T223, tree(T277, T278, T279))) → U8_ag(T280, T222, T223, T277, T278, T279, tree_memberA_in_ag(T280, T279))
U8_ag(T280, T222, T223, T277, T278, T279, tree_memberA_out_ag(T280, T279)) → tree_memberA_out_ag(T280, tree(T222, T223, tree(T277, T278, T279)))
U7_ag(T261, T222, T223, T258, T259, T260, tree_memberA_out_ag(T261, T259)) → tree_memberA_out_ag(T261, tree(T222, T223, tree(T258, T259, T260)))
U6_ag(T210, T207, T208, T209, tree_memberA_out_ag(T210, T209)) → tree_memberA_out_ag(T210, tree(T207, T208, T209))
U5_ag(T184, T118, T181, T182, T183, T120, tree_memberA_out_ag(T184, T183)) → tree_memberA_out_ag(T184, tree(T118, tree(T181, T182, T183), T120))
U4_ag(T157, T118, T154, T155, T156, T120, tree_memberA_out_ag(T157, T155)) → tree_memberA_out_ag(T157, tree(T118, tree(T154, T155, T156), T120))
U3_ag(T106, T103, T104, T105, tree_memberA_out_ag(T106, T105)) → tree_memberA_out_ag(T106, tree(T103, T104, T105))
U2_ag(T80, T14, T77, T78, T79, T16, tree_memberA_out_ag(T80, T79)) → tree_memberA_out_ag(T80, tree(T14, tree(T77, T78, T79), T16))
U1_ag(T53, T14, T50, T51, T52, T16, tree_memberA_out_ag(T53, T51)) → tree_memberA_out_ag(T53, tree(T14, tree(T50, T51, T52), T16))

The argument filtering Pi contains the following mapping:
tree_memberA_in_ag(x1, x2)  =  tree_memberA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
tree_memberA_out_ag(x1, x2)  =  tree_memberA_out_ag(x1)
U1_ag(x1, x2, x3, x4, x5, x6, x7)  =  U1_ag(x7)
U2_ag(x1, x2, x3, x4, x5, x6, x7)  =  U2_ag(x7)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x5)
U4_ag(x1, x2, x3, x4, x5, x6, x7)  =  U4_ag(x7)
U5_ag(x1, x2, x3, x4, x5, x6, x7)  =  U5_ag(x7)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x5)
U7_ag(x1, x2, x3, x4, x5, x6, x7)  =  U7_ag(x7)
U8_ag(x1, x2, x3, x4, x5, x6, x7)  =  U8_ag(x7)
TREE_MEMBERA_IN_AG(x1, x2)  =  TREE_MEMBERA_IN_AG(x2)
U1_AG(x1, x2, x3, x4, x5, x6, x7)  =  U1_AG(x7)
U2_AG(x1, x2, x3, x4, x5, x6, x7)  =  U2_AG(x7)
U3_AG(x1, x2, x3, x4, x5)  =  U3_AG(x5)
U4_AG(x1, x2, x3, x4, x5, x6, x7)  =  U4_AG(x7)
U5_AG(x1, x2, x3, x4, x5, x6, x7)  =  U5_AG(x7)
U6_AG(x1, x2, x3, x4, x5)  =  U6_AG(x5)
U7_AG(x1, x2, x3, x4, x5, x6, x7)  =  U7_AG(x7)
U8_AG(x1, x2, x3, x4, x5, x6, x7)  =  U8_AG(x7)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TREE_MEMBERA_IN_AG(T53, tree(T14, tree(T50, T51, T52), T16)) → U1_AG(T53, T14, T50, T51, T52, T16, tree_memberA_in_ag(T53, T51))
TREE_MEMBERA_IN_AG(T53, tree(T14, tree(T50, T51, T52), T16)) → TREE_MEMBERA_IN_AG(T53, T51)
TREE_MEMBERA_IN_AG(T80, tree(T14, tree(T77, T78, T79), T16)) → U2_AG(T80, T14, T77, T78, T79, T16, tree_memberA_in_ag(T80, T79))
TREE_MEMBERA_IN_AG(T80, tree(T14, tree(T77, T78, T79), T16)) → TREE_MEMBERA_IN_AG(T80, T79)
TREE_MEMBERA_IN_AG(T106, tree(T103, T104, T105)) → U3_AG(T106, T103, T104, T105, tree_memberA_in_ag(T106, T105))
TREE_MEMBERA_IN_AG(T106, tree(T103, T104, T105)) → TREE_MEMBERA_IN_AG(T106, T105)
TREE_MEMBERA_IN_AG(T157, tree(T118, tree(T154, T155, T156), T120)) → U4_AG(T157, T118, T154, T155, T156, T120, tree_memberA_in_ag(T157, T155))
TREE_MEMBERA_IN_AG(T184, tree(T118, tree(T181, T182, T183), T120)) → U5_AG(T184, T118, T181, T182, T183, T120, tree_memberA_in_ag(T184, T183))
TREE_MEMBERA_IN_AG(T210, tree(T207, T208, T209)) → U6_AG(T210, T207, T208, T209, tree_memberA_in_ag(T210, T209))
TREE_MEMBERA_IN_AG(T261, tree(T222, T223, tree(T258, T259, T260))) → U7_AG(T261, T222, T223, T258, T259, T260, tree_memberA_in_ag(T261, T259))
TREE_MEMBERA_IN_AG(T261, tree(T222, T223, tree(T258, T259, T260))) → TREE_MEMBERA_IN_AG(T261, T259)
TREE_MEMBERA_IN_AG(T280, tree(T222, T223, tree(T277, T278, T279))) → U8_AG(T280, T222, T223, T277, T278, T279, tree_memberA_in_ag(T280, T279))
TREE_MEMBERA_IN_AG(T280, tree(T222, T223, tree(T277, T278, T279))) → TREE_MEMBERA_IN_AG(T280, T279)

The TRS R consists of the following rules:

tree_memberA_in_ag(T6, tree(T6, T7, T8)) → tree_memberA_out_ag(T6, tree(T6, T7, T8))
tree_memberA_in_ag(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_memberA_out_ag(T30, tree(T14, tree(T30, T31, T32), T16))
tree_memberA_in_ag(T53, tree(T14, tree(T50, T51, T52), T16)) → U1_ag(T53, T14, T50, T51, T52, T16, tree_memberA_in_ag(T53, T51))
tree_memberA_in_ag(T80, tree(T14, tree(T77, T78, T79), T16)) → U2_ag(T80, T14, T77, T78, T79, T16, tree_memberA_in_ag(T80, T79))
tree_memberA_in_ag(T106, tree(T103, T104, T105)) → U3_ag(T106, T103, T104, T105, tree_memberA_in_ag(T106, T105))
tree_memberA_in_ag(T157, tree(T118, tree(T154, T155, T156), T120)) → U4_ag(T157, T118, T154, T155, T156, T120, tree_memberA_in_ag(T157, T155))
tree_memberA_in_ag(T184, tree(T118, tree(T181, T182, T183), T120)) → U5_ag(T184, T118, T181, T182, T183, T120, tree_memberA_in_ag(T184, T183))
tree_memberA_in_ag(T210, tree(T207, T208, T209)) → U6_ag(T210, T207, T208, T209, tree_memberA_in_ag(T210, T209))
tree_memberA_in_ag(T238, tree(T222, T223, tree(T238, T239, T240))) → tree_memberA_out_ag(T238, tree(T222, T223, tree(T238, T239, T240)))
tree_memberA_in_ag(T261, tree(T222, T223, tree(T258, T259, T260))) → U7_ag(T261, T222, T223, T258, T259, T260, tree_memberA_in_ag(T261, T259))
tree_memberA_in_ag(T280, tree(T222, T223, tree(T277, T278, T279))) → U8_ag(T280, T222, T223, T277, T278, T279, tree_memberA_in_ag(T280, T279))
U8_ag(T280, T222, T223, T277, T278, T279, tree_memberA_out_ag(T280, T279)) → tree_memberA_out_ag(T280, tree(T222, T223, tree(T277, T278, T279)))
U7_ag(T261, T222, T223, T258, T259, T260, tree_memberA_out_ag(T261, T259)) → tree_memberA_out_ag(T261, tree(T222, T223, tree(T258, T259, T260)))
U6_ag(T210, T207, T208, T209, tree_memberA_out_ag(T210, T209)) → tree_memberA_out_ag(T210, tree(T207, T208, T209))
U5_ag(T184, T118, T181, T182, T183, T120, tree_memberA_out_ag(T184, T183)) → tree_memberA_out_ag(T184, tree(T118, tree(T181, T182, T183), T120))
U4_ag(T157, T118, T154, T155, T156, T120, tree_memberA_out_ag(T157, T155)) → tree_memberA_out_ag(T157, tree(T118, tree(T154, T155, T156), T120))
U3_ag(T106, T103, T104, T105, tree_memberA_out_ag(T106, T105)) → tree_memberA_out_ag(T106, tree(T103, T104, T105))
U2_ag(T80, T14, T77, T78, T79, T16, tree_memberA_out_ag(T80, T79)) → tree_memberA_out_ag(T80, tree(T14, tree(T77, T78, T79), T16))
U1_ag(T53, T14, T50, T51, T52, T16, tree_memberA_out_ag(T53, T51)) → tree_memberA_out_ag(T53, tree(T14, tree(T50, T51, T52), T16))

The argument filtering Pi contains the following mapping:
tree_memberA_in_ag(x1, x2)  =  tree_memberA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
tree_memberA_out_ag(x1, x2)  =  tree_memberA_out_ag(x1)
U1_ag(x1, x2, x3, x4, x5, x6, x7)  =  U1_ag(x7)
U2_ag(x1, x2, x3, x4, x5, x6, x7)  =  U2_ag(x7)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x5)
U4_ag(x1, x2, x3, x4, x5, x6, x7)  =  U4_ag(x7)
U5_ag(x1, x2, x3, x4, x5, x6, x7)  =  U5_ag(x7)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x5)
U7_ag(x1, x2, x3, x4, x5, x6, x7)  =  U7_ag(x7)
U8_ag(x1, x2, x3, x4, x5, x6, x7)  =  U8_ag(x7)
TREE_MEMBERA_IN_AG(x1, x2)  =  TREE_MEMBERA_IN_AG(x2)
U1_AG(x1, x2, x3, x4, x5, x6, x7)  =  U1_AG(x7)
U2_AG(x1, x2, x3, x4, x5, x6, x7)  =  U2_AG(x7)
U3_AG(x1, x2, x3, x4, x5)  =  U3_AG(x5)
U4_AG(x1, x2, x3, x4, x5, x6, x7)  =  U4_AG(x7)
U5_AG(x1, x2, x3, x4, x5, x6, x7)  =  U5_AG(x7)
U6_AG(x1, x2, x3, x4, x5)  =  U6_AG(x5)
U7_AG(x1, x2, x3, x4, x5, x6, x7)  =  U7_AG(x7)
U8_AG(x1, x2, x3, x4, x5, x6, x7)  =  U8_AG(x7)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 8 less nodes.

(8) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TREE_MEMBERA_IN_AG(T80, tree(T14, tree(T77, T78, T79), T16)) → TREE_MEMBERA_IN_AG(T80, T79)
TREE_MEMBERA_IN_AG(T53, tree(T14, tree(T50, T51, T52), T16)) → TREE_MEMBERA_IN_AG(T53, T51)
TREE_MEMBERA_IN_AG(T106, tree(T103, T104, T105)) → TREE_MEMBERA_IN_AG(T106, T105)
TREE_MEMBERA_IN_AG(T261, tree(T222, T223, tree(T258, T259, T260))) → TREE_MEMBERA_IN_AG(T261, T259)
TREE_MEMBERA_IN_AG(T280, tree(T222, T223, tree(T277, T278, T279))) → TREE_MEMBERA_IN_AG(T280, T279)

The TRS R consists of the following rules:

tree_memberA_in_ag(T6, tree(T6, T7, T8)) → tree_memberA_out_ag(T6, tree(T6, T7, T8))
tree_memberA_in_ag(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_memberA_out_ag(T30, tree(T14, tree(T30, T31, T32), T16))
tree_memberA_in_ag(T53, tree(T14, tree(T50, T51, T52), T16)) → U1_ag(T53, T14, T50, T51, T52, T16, tree_memberA_in_ag(T53, T51))
tree_memberA_in_ag(T80, tree(T14, tree(T77, T78, T79), T16)) → U2_ag(T80, T14, T77, T78, T79, T16, tree_memberA_in_ag(T80, T79))
tree_memberA_in_ag(T106, tree(T103, T104, T105)) → U3_ag(T106, T103, T104, T105, tree_memberA_in_ag(T106, T105))
tree_memberA_in_ag(T157, tree(T118, tree(T154, T155, T156), T120)) → U4_ag(T157, T118, T154, T155, T156, T120, tree_memberA_in_ag(T157, T155))
tree_memberA_in_ag(T184, tree(T118, tree(T181, T182, T183), T120)) → U5_ag(T184, T118, T181, T182, T183, T120, tree_memberA_in_ag(T184, T183))
tree_memberA_in_ag(T210, tree(T207, T208, T209)) → U6_ag(T210, T207, T208, T209, tree_memberA_in_ag(T210, T209))
tree_memberA_in_ag(T238, tree(T222, T223, tree(T238, T239, T240))) → tree_memberA_out_ag(T238, tree(T222, T223, tree(T238, T239, T240)))
tree_memberA_in_ag(T261, tree(T222, T223, tree(T258, T259, T260))) → U7_ag(T261, T222, T223, T258, T259, T260, tree_memberA_in_ag(T261, T259))
tree_memberA_in_ag(T280, tree(T222, T223, tree(T277, T278, T279))) → U8_ag(T280, T222, T223, T277, T278, T279, tree_memberA_in_ag(T280, T279))
U8_ag(T280, T222, T223, T277, T278, T279, tree_memberA_out_ag(T280, T279)) → tree_memberA_out_ag(T280, tree(T222, T223, tree(T277, T278, T279)))
U7_ag(T261, T222, T223, T258, T259, T260, tree_memberA_out_ag(T261, T259)) → tree_memberA_out_ag(T261, tree(T222, T223, tree(T258, T259, T260)))
U6_ag(T210, T207, T208, T209, tree_memberA_out_ag(T210, T209)) → tree_memberA_out_ag(T210, tree(T207, T208, T209))
U5_ag(T184, T118, T181, T182, T183, T120, tree_memberA_out_ag(T184, T183)) → tree_memberA_out_ag(T184, tree(T118, tree(T181, T182, T183), T120))
U4_ag(T157, T118, T154, T155, T156, T120, tree_memberA_out_ag(T157, T155)) → tree_memberA_out_ag(T157, tree(T118, tree(T154, T155, T156), T120))
U3_ag(T106, T103, T104, T105, tree_memberA_out_ag(T106, T105)) → tree_memberA_out_ag(T106, tree(T103, T104, T105))
U2_ag(T80, T14, T77, T78, T79, T16, tree_memberA_out_ag(T80, T79)) → tree_memberA_out_ag(T80, tree(T14, tree(T77, T78, T79), T16))
U1_ag(T53, T14, T50, T51, T52, T16, tree_memberA_out_ag(T53, T51)) → tree_memberA_out_ag(T53, tree(T14, tree(T50, T51, T52), T16))

The argument filtering Pi contains the following mapping:
tree_memberA_in_ag(x1, x2)  =  tree_memberA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
tree_memberA_out_ag(x1, x2)  =  tree_memberA_out_ag(x1)
U1_ag(x1, x2, x3, x4, x5, x6, x7)  =  U1_ag(x7)
U2_ag(x1, x2, x3, x4, x5, x6, x7)  =  U2_ag(x7)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x5)
U4_ag(x1, x2, x3, x4, x5, x6, x7)  =  U4_ag(x7)
U5_ag(x1, x2, x3, x4, x5, x6, x7)  =  U5_ag(x7)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x5)
U7_ag(x1, x2, x3, x4, x5, x6, x7)  =  U7_ag(x7)
U8_ag(x1, x2, x3, x4, x5, x6, x7)  =  U8_ag(x7)
TREE_MEMBERA_IN_AG(x1, x2)  =  TREE_MEMBERA_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(9) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(10) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TREE_MEMBERA_IN_AG(T80, tree(T14, tree(T77, T78, T79), T16)) → TREE_MEMBERA_IN_AG(T80, T79)
TREE_MEMBERA_IN_AG(T53, tree(T14, tree(T50, T51, T52), T16)) → TREE_MEMBERA_IN_AG(T53, T51)
TREE_MEMBERA_IN_AG(T106, tree(T103, T104, T105)) → TREE_MEMBERA_IN_AG(T106, T105)
TREE_MEMBERA_IN_AG(T261, tree(T222, T223, tree(T258, T259, T260))) → TREE_MEMBERA_IN_AG(T261, T259)
TREE_MEMBERA_IN_AG(T280, tree(T222, T223, tree(T277, T278, T279))) → TREE_MEMBERA_IN_AG(T280, T279)

R is empty.
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
TREE_MEMBERA_IN_AG(x1, x2)  =  TREE_MEMBERA_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(11) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TREE_MEMBERA_IN_AG(tree(T14, tree(T77, T78, T79), T16)) → TREE_MEMBERA_IN_AG(T79)
TREE_MEMBERA_IN_AG(tree(T14, tree(T50, T51, T52), T16)) → TREE_MEMBERA_IN_AG(T51)
TREE_MEMBERA_IN_AG(tree(T103, T104, T105)) → TREE_MEMBERA_IN_AG(T105)
TREE_MEMBERA_IN_AG(tree(T222, T223, tree(T258, T259, T260))) → TREE_MEMBERA_IN_AG(T259)
TREE_MEMBERA_IN_AG(tree(T222, T223, tree(T277, T278, T279))) → TREE_MEMBERA_IN_AG(T279)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(13) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• TREE_MEMBERA_IN_AG(tree(T14, tree(T77, T78, T79), T16)) → TREE_MEMBERA_IN_AG(T79)
  The graph contains the following edges 1 > 1

• TREE_MEMBERA_IN_AG(tree(T14, tree(T50, T51, T52), T16)) → TREE_MEMBERA_IN_AG(T51)
  The graph contains the following edges 1 > 1

• TREE_MEMBERA_IN_AG(tree(T103, T104, T105)) → TREE_MEMBERA_IN_AG(T105)
  The graph contains the following edges 1 > 1

• TREE_MEMBERA_IN_AG(tree(T222, T223, tree(T258, T259, T260))) → TREE_MEMBERA_IN_AG(T259)
  The graph contains the following edges 1 > 1

• TREE_MEMBERA_IN_AG(tree(T222, T223, tree(T277, T278, T279))) → TREE_MEMBERA_IN_AG(T279)
  The graph contains the following edges 1 > 1

(14) YES